Inference at * 2 2 
Iof proof for Lemma member nth tl:



1. T : Type
2. n : 
3. 0 < n
4. x:T, L:(T List). (x  nth_tl(n - 1;L))  (x  L)
5. x : T
6. T List
7. u : T
8. v : T List
9. (x  nth_tl(n;v))  (x  v)
  (x  nth_tl(n;[u / v]))  (x  [u / v]) 

latex

 by ((RecUnfold `nth_tl` 0) 
CollapseTHEN ((((if (0) =0 then SplitOnConclITE else SplitOnHypITE (0
C))) 
CollapseTHENA (Auto)))) 

latex

C1: .....truecase..... NILNIL

C1: 10. n  0
C1:   (x  [u / v])  (x  [u / v])
C2: .....falsecase..... NILNIL

C2: 10. 0 < n
C2:   (x  nth_tl(n - 1;tl([u / v])))  (x  [u / v])
C.

Definitions	left + right, Unit, p q, p  q, p  q, [d], a < b, x f y, f(a), a < b, null(as), x =a y, (i = j), A, P  Q, T, P  Q, P & Q, x:A  B(x), tt, A  B, True, t  T, b, b, i <z j, , i z j, #$n, ff, P  Q, type List, x:A. B(x), x:AB(x), a < b, , s = t, , Type
Lemmas	eqtt to assert, assert of le int, iff transitivity, eqff to assert, iff wf, rev implies wf, squash wf, true wf, bnot of le int, assert of lt int, le int wf, le wf, bool wf, lt int wf, assert wf, bnot wf